$\forall$${\it ds}$:fpf(Id; $x$.Type), ${\it da}$:fpf(Knd; $k$.Type), ${\it snd}$:msg{-}spec(${\it ds}$; ${\it da}$). \\[0ex]msg{-}spec{-}links(${\it snd}$) $\in$ (IdLnk List)